$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)). p{-}id() o $f$   = $f$